\begin{tabbing}
w{-}machine{-}constraint($w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:Id.\+
\\[0ex]let ${\it Choose}$,${\it Trans}$,${\it Send}$ = w{-}machine($w$;$i$) in 
\\[0ex]$\forall$$t$:$\mathbb{N}$.
\\[0ex]$\neg$isnull(a($i$;$t$))
\\[0ex]$\Rightarrow$ \=($\lambda$$x$.s($i$;$t$+1).$x$) $=$ ${\it Trans}$(kind(a($i$;$t$)),val(a($i$;$t$)),$\lambda$$x$.s($i$;$t$).$x$)\+
\\[0ex]\& (\=islocal(kind(a($i$;$t$)))\+
\\[0ex]$\Rightarrow$ \=isl(${\it Choose}$(act(kind(a($i$;$t$))),$\lambda$$x$.s($i$;$t$).$x$))\+
\\[0ex]\& val(a($i$;$t$)) $=$ outl(${\it Choose}$(act(kind(a($i$;$t$))),$\lambda$$x$.s($i$;$t$).$x$)))
\-\-\\[0ex]\& m($i$;$t$) $=$ ${\it Send}$(kind(a($i$;$t$)),val(a($i$;$t$)),$\lambda$$x$.s($i$;$t$).$x$)
\-\-
\end{tabbing}